Runtime verification is an effective automated method for specification-basedoffline testing and analysis as well as online monitoring of complex systems.The specification language is often a variant of regular expressions or apopular temporal logic, such as LTL. This paper presents a novel and efficientparallel algorithm for verifying a more expressive version of LTLspecifications that incorporates counting semantics, where nested quantifierscan be subject to numerical constraints. Such constraints are useful inevaluating thresholds (e.g., expected uptime of a web server). The significanceof this extension is that it enables us to reason about the correctness of alarge class of systems, such as web servers, OS kernels, and network behavior,where properties are required to be instantiated for parameterized requests,kernel objects, network nodes, etc. Our algorithm uses the popular {\emMapReduce} architecture to split a program trace into variable-based clustersat run time. Each cluster is then mapped to its respective monitor instances,verified, and reduced collectively on a multi-core CPU or the GPU. Ouralgorithm is fully implemented and we report very encouraging experimentalresults, where the monitoring overhead is negligible on real-world data sets.
展开▼
